Section: Software

Apron and BddApron Libraries

Participant : Bertrand Jeannet.

Principles

The Apron library (http://apron.cri.ensmp.fr/library/ ) is dedicated to the static analysis of the numerical variables of a program by abstract interpretation [43] . Many abstract domains have been designed and implemented for analysing the possible values of numerical variables during the execution of a program (see Figure 1 ). However, their API diverge largely (datatypes, signatures, ...), and this does not ease their diffusion and experimental comparison w.r.t. efficiency and precision aspects.

The Apron library provides:

• a uniform API for existing numerical abstract domains;

• a higher-level interface to the client tools, by factorizing functionalities that are largely independent of abstract domains.

From an abstract domain designer point of view, the benefits of the Apron library are:

• the ability to focus on core, low-level functionalities;

• the help of generic services adding higher-level services for free.

For the client static analysis community, the benefits are a unified, higher-level interface, which allows experimenting, comparing, and combining abstract domains.

In 2011, the Taylor1plus domain [53] , which is the underlying abstract domain of the tool Fluctuat [51] has been improved. Glue code has also been added to enable the connection of an abstract domain implemented in OCaml to the Apron infrastructure written in C (this requires callbacks from C to OCaml that are safe w.r.t. garbage collection). This will enable the integration in Apron of the MaxPlus polyhedra library written by X. Allamigeon [30] in the context of the ANR Asopt project.

Figure 1. Typical static analyser and examples of abstract domains

The BddApron library (http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/bddapron/index.html ) aims at a similar goal, by adding finite-types variables and expressions to the concrete semantics of Apron domains. It is built upon the Apron library and provides abstract domains for the combination of finite-type variables (Booleans, enumerated types, bitvectors) and numerical variables (integers, rationals, floating-point numbers). It first allows the manipulation of expressions that freely mix, using BDDs and MTBDDs, finite-type and numerical Apron expressions and conditions. It then provides abstract domains that combines BDDs and Apron abstract values for representing invariants holding on both finite-type variables and numerical variables.

Implementation and Distribution

The Apron library (Fig. 2 ) is written in ANSI C, with an object-oriented and thread-safe design. Both multi-precision and floating-point numbers are supported. A wrapper for the Ocaml language is available, and a C++ wrapper is on the way. It has been distributed since June 2006 under the LGPL license and available at http://apron.cri.ensmp.fr . Its development has still progressed much since. There are already many external users (ProVal/Démons, LRI Orsay, France — CEA-LIST, Saclay, France — Analysis of Computer Systems Group, New-York University, USA — Sierum software analysis platform, Kansas State University, USA — NEC Labs, Princeton, USA — EADS CCR, Paris, France — IRIT, Toulouse, France) and is currently packaged as a Redhat and Debian package.

The BddApron library is written in Ocaml , using polymorphism features of Ocaml to make it generic. It is also thread-safe. It provides two different implementations of the same domain, each one presenting pros and cons depending on the application. It is currently used by the ConcurInterproc interprocedural and concurrent program analyzer.

Figure 2. Organisation of the Apron library